\begin{tabbing}
$a$(v) sends [${\it tg}$,   $f$($x$, v)] on link $l$  
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=with declarations \+
\\[0ex]ds:$x$ : $A$
\\[0ex]da:$a$ : $B$ $\oplus$ rcv($l$,${\it tg}$) : $T$
\\[0ex]$a$(v) sends [$\langle$${\it tg}$$,\,$$\lambda$$s$,$v$. $f$($s$($x$),$v$)$\rangle$] s v on link $l$
\-
\end{tabbing}